We present an algorithm for synthesising a controller (supervisor) for adiscrete event system (DES) based on the property-directed reachability (PDR)model checking algorithm. The discrete event systems framework is useful inboth software, automation and manufacturing, as problems from those domains canbe modelled as discrete supervisory control problems. As a formal framework,DES is also similar to domains for which the field of formal methods forcomputer science has developed techniques and tools. In this paper, we attemptto marry the two by adapting PDR to the problem of controller synthesis. Theresulting algorithm takes as input a transition system with forbidden statesand uncontrollable transitions, and synthesises a safe andminimally-restrictive controller, correct-by-design. We also present animplementation along with experimental results, showing that the algorithm haspotential as a part of the solution to the greater effort of formal supervisorycontroller synthesis and verification.
展开▼
